T:Type, L1, L:T List. interleaving(T;L1;nil;L)  L = L1 

latex

Definitions	disjoint_sublists(T;L1;L2;L), Prop, t  T, x:A. B(x), , {T}, P  Q, SQType(T), P & Q, P  Q, ij, ||as||, AB, False, A, P  Q, interleaving(T;L1;L2;L), True, T, {i..j}, l[i], S  T, S  T, increasing(f;k), x:A. B(x), i  j < k
Lemmas	increasing wf, int seg wf, select wf, not wf, length wf2, id increasing, proper sublist length, disjoint sublists sublist, nat wf, le wf, length wf1, non neg length, cons one one, disjoint sublists wf, member wf